[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification MAKS-BSRA-unwinding
enrich eventfuns with
   constants 
      xosc : bool; comment: output step consistency.;
      xlrf : bool; comment: locally-respects forwards.;
      validx : bool; comment: eqrel is an equivalence relation on C, and Cs are related only to other Cs.;
   functions 
      view : event → viewstate;
   predicates 
      eqrel : event × event;
      eqstate : state × state;
   
   axioms 
      eqstate-reflexive :  ⊦ ∀ s. eqstate(s, s);
      validx-def
      : ⊦ 
          validx
        ↔   (∀ ev. view(ev) = C → eqrel(ev, ev)) ∧ (∀ ev, ev0. view(ev) = C ∧ view(ev0) = C ∧ eqrel(ev, ev0) → eqrel(ev0, ev))
          ∧ (∀ ev, ev0, ev1. view(ev) = C ∧ view(ev0) = C ∧ view(ev1) = C ∧ eqrel(ev, ev0) ∧ eqrel(ev0, ev1) → eqrel(ev, ev1))
          ∧ (∀ ev, ev0. view(ev) = C ∧ eqrel(ev, ev0) → view(ev0) = C) ∧ (∀ ev, ev0. view(ev0) = C ∧ eqrel(ev, ev0) → view(ev) = C);
      comment: eqrel is an equivalence relation on C, and Cs are related only to other Cs.;
       
      xosc-def
      : ⊦ 
          xosc
        ↔ (∀ s1, s11, s22. 
            ∀ ev. 
               view(ev) ≠ C ∧ reachable(s1) ∧ reachable(s11) ∧ trans(s11, ev, s22) ∧ eqstate(s11, s1)
             → (∃ s2. ∃ tr. proj(tr, Cview(view)) = [] ∧ proj(tr, Vview(view)) = proj(ev ', Vview(view)) ∧ trans∃(s1, tr, s2) ∧ eqstate(s22, s2)));
      xlrf-def
      : ⊦ 
          xlrf
        ↔ (∀ s, s0, s1. 
            ∀ ev, ev0. 
               view(ev) = C ∧ view(ev0) = C ∧ eqrel(ev, ev0) ∧ reachable(s) ∧ trans(s, ev, s0) ∧ eqstate(s, s1) ∧ reachable(s1)
             → (∃ s2. trans(s1, ev0, s2) ∧ eqstate(s0, s2)));
end enrich